Charlie is green. Charlie is quiet. Erin is big. Erin is nice. Erin is rough. Gary is big. Gary is green. Gary is red. Gary is rough. Gary is smart. All red people are rough. Big, green people are rough. If someone is red then they are quiet. Green people are smart. All nice, big people are red. All quiet people are green.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Big, green people are rough.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is red then they are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
All nice, big people are red.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Erin is big.
True
1
proof
[(triple3)]
("Erin" "is" "big" "+")
triple3
Gary is not green.
False
1
inv-proof
[(triple7 OR ((((triple8) -> rule3)) -> rule6))]
("Gary" "is" "green" "-")
triple7
((((triple8) -> (rule3 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Charlie is not rough.
Unknown
inv-rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is green.[(triple1 OR ((triple2) -> rule6))] Charlie is quiet.[(triple2)] Erin is big.[(triple3)] Erin is nice.[(triple4)] Erin is rough.[(triple5 OR ((((triple4 triple3) -> rule5)) -> rule1) OR ((triple3 ((((((triple4 triple3) -> rule5)) -> rule3)) -> rule6)) -> rule2))] Gary is big.[(triple6)] Gary is green.[(triple7 OR ((((triple8) -> rule3)) -> rule6))] Gary is red.[(triple8)] Gary is rough.[(triple9 OR ((triple8) -> rule1) OR ((triple6 triple7) -> rule2) OR ((triple6 ((((triple8) -> rule3)) -> rule6)) -> rule2))] Gary is smart.[(triple10 OR ((triple7) -> rule4) OR ((((((triple8) -> rule3)) -> rule6)) -> rule4))] @1: Charlie is smart.[(((triple1) -> rule4) OR ((((triple2) -> rule6)) -> rule4))] Erin is red.[(((triple4 triple3) -> rule5))] Gary is quiet.[(((triple8) -> rule3))] @2: Erin is quiet.[(((((triple4 triple3) -> rule5)) -> rule3))] @3: Erin is green.[(((((((triple4 triple3) -> rule5)) -> rule3)) -> rule6))] @4: Erin is smart.[(((((((((triple4 triple3) -> rule5)) -> rule3)) -> rule6)) -> rule4))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
((triple2) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
((((triple4 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((triple3 ((((((triple4 triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((((triple8) -> (rule3 % int2))) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
((triple8) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple6 triple7) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple6 ((((triple8) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
triple10
((triple7) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((((triple8) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple4 triple3) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple8) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple4 triple3) -> (rule5 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((((((triple4 triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((((((((triple4 triple3) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4