Anne is green. Bob is blue. Charlie is rough. Gary is red. If Bob is green then Bob is rough. All green people are red. Blue people are smart. If Anne is not big then Anne is rough. All blue, smart people are green. If someone is smart and not rough then they are kind.
Anne is green.
("Anne" "is" "green" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Gary is red.
("Gary" "is" "red" "+")
If Bob is green then Bob is rough.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "rough" "+"))
All green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If Anne is not big then Anne is rough.
((("Anne" "is" "big" "~")) -> ("Anne" "is" "rough" "+"))
All blue, smart people are green.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and not rough then they are kind.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "kind" "+"))
Anne is green.
True
1
proof
[(triple1)]
("Anne" "is" "green" "+")
triple1
Charlie is not rough.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "rough" "-")
triple3
Anne is red.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "red" "+")
((triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "red" "-")
((triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is green.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule5))]
("Bob" "is" "green" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not green.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule5))]
("Bob" "is" "green" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is red.
True
5
proof
[(((((triple2 ((triple2) -> rule3)) -> rule5)) -> rule2))]
("Bob" "is" "red" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not rough.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule3)) -> rule5)) -> rule1))]
("Bob" "is" "rough" "-")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "kind" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "kind" "+")
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "kind" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "green" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Anne is green.[(triple1)] Bob is blue.[(triple2)] Charlie is rough.[(triple3)] Gary is red.[(triple4)] @1: Anne is red.[(((triple1) -> rule2))] Bob is smart.[(((triple2) -> rule3))] @2: Bob is green.[(((triple2 ((triple2) -> rule3)) -> rule5))] @3: Bob is red.[(((((triple2 ((triple2) -> rule3)) -> rule5)) -> rule2))] Bob is rough.[(((((triple2 ((triple2) -> rule3)) -> rule5)) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3