Charlie is green. Charlie is kind. Charlie is quiet. Charlie is red. Charlie is rough. Fiona is quiet. Fiona is white. Gary is cold. Gary is green. Gary is quiet. Gary is red. Gary is rough. Gary is white. Harry is kind. Harry is quiet. Harry is rough. Green people are kind. All red, quiet people are rough. Cold, green people are rough. If Fiona is cold then Fiona is green. White people are cold. If Charlie is green and Charlie is rough then Charlie is kind. Green, rough people are kind. Red people are quiet.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
All red, quiet people are rough.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Cold, green people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If Fiona is cold then Fiona is green.
((("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "green" "+"))
White people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is green and Charlie is rough then Charlie is kind.
((("Charlie" "is" "green" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "kind" "+"))
Green, rough people are kind.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is rough.
True
1
proof
[(triple5 OR ((triple4 triple3) -> rule2) OR ((triple4 ((triple4) -> rule8)) -> rule2))]
("Charlie" "is" "rough" "+")
triple5
((triple4 triple3) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple4 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not kind.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule1) OR ((triple1 triple5) -> rule6) OR ((triple1 triple5) -> rule7) OR ((triple1 ((triple4 triple3) -> rule2)) -> rule6) OR ((triple1 ((triple4 triple3) -> rule2)) -> rule7) OR ((triple1 ((triple4 ((triple4) -> rule8)) -> rule2)) -> rule6) OR ((triple1 ((triple4 ((triple4) -> rule8)) -> rule2)) -> rule7))]
("Charlie" "is" "kind" "-")
triple2
((triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple1 triple5) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple1 triple5) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple1 ((triple4 triple3) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((triple1 ((triple4 triple3) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((triple1 ((triple4 ((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((triple1 ((triple4 ((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Gary is kind.
True
2
proof
[(((triple9) -> rule1) OR ((triple9 triple12) -> rule7) OR ((triple9 ((triple11 triple10) -> rule2)) -> rule7) OR ((triple9 ((triple8 triple9) -> rule3)) -> rule7) OR ((triple9 ((triple11 ((triple11) -> rule8)) -> rule2)) -> rule7) OR ((triple9 ((((triple13) -> rule5) triple9) -> rule3)) -> rule7))]
("Gary" "is" "kind" "+")
((triple9) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple9 triple12) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple9 ((triple11 triple10) -> (rule2 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple9 ((triple8 triple9) -> (rule3 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple9 ((triple11 ((triple11) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((triple9 ((((triple13) -> (rule5 % int3)) triple9) -> (rule3 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is not kind.
False
2
inv-proof
[(((triple9) -> rule1) OR ((triple9 triple12) -> rule7) OR ((triple9 ((triple11 triple10) -> rule2)) -> rule7) OR ((triple9 ((triple8 triple9) -> rule3)) -> rule7) OR ((triple9 ((triple11 ((triple11) -> rule8)) -> rule2)) -> rule7) OR ((triple9 ((((triple13) -> rule5) triple9) -> rule3)) -> rule7))]
("Gary" "is" "kind" "-")
((triple9) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple9 triple12) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple9 ((triple11 triple10) -> (rule2 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple9 ((triple8 triple9) -> (rule3 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple9 ((triple11 ((triple11) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((triple9 ((((triple13) -> (rule5 % int3)) triple9) -> (rule3 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "cold" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "cold" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is green.[(triple1)] Charlie is kind.[(triple2 OR ((triple1) -> rule1) OR ((triple1 triple5) -> rule6) OR ((triple1 triple5) -> rule7) OR ((triple1 ((triple4 triple3) -> rule2)) -> rule6) OR ((triple1 ((triple4 triple3) -> rule2)) -> rule7) OR ((triple1 ((triple4 ((triple4) -> rule8)) -> rule2)) -> rule6) OR ((triple1 ((triple4 ((triple4) -> rule8)) -> rule2)) -> rule7))] Charlie is quiet.[(triple3 OR ((triple4) -> rule8))] Charlie is red.[(triple4)] Charlie is rough.[(triple5 OR ((triple4 triple3) -> rule2) OR ((triple4 ((triple4) -> rule8)) -> rule2))] Fiona is quiet.[(triple6)] Fiona is white.[(triple7)] Gary is cold.[(triple8 OR ((triple13) -> rule5))] Gary is green.[(triple9)] Gary is quiet.[(triple10 OR ((triple11) -> rule8))] Gary is red.[(triple11)] Gary is rough.[(triple12 OR ((triple11 triple10) -> rule2) OR ((triple8 triple9) -> rule3) OR ((triple11 ((triple11) -> rule8)) -> rule2) OR ((((triple13) -> rule5) triple9) -> rule3))] Gary is white.[(triple13)] Harry is kind.[(triple14)] Harry is quiet.[(triple15)] Harry is rough.[(triple16)] @1: Fiona is cold.[(((triple7) -> rule5))] Gary is kind.[(((triple9) -> rule1) OR ((triple9 triple12) -> rule7) OR ((triple9 ((triple11 triple10) -> rule2)) -> rule7) OR ((triple9 ((triple8 triple9) -> rule3)) -> rule7) OR ((triple9 ((triple11 ((triple11) -> rule8)) -> rule2)) -> rule7) OR ((triple9 ((((triple13) -> rule5) triple9) -> rule3)) -> rule7))] @2: Fiona is green.[(((((triple7) -> rule5)) -> rule4))] @3: Fiona is kind.[(((((((triple7) -> rule5)) -> rule4)) -> rule1) OR ((((((triple7) -> rule5)) -> rule4) ((((triple7) -> rule5) ((((triple7) -> rule5)) -> rule4)) -> rule3)) -> rule7))] Fiona is rough.[(((((triple7) -> rule5) ((((triple7) -> rule5)) -> rule4)) -> rule3))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple1 triple5) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple1 triple5) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple1 ((triple4 triple3) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((triple1 ((triple4 triple3) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((triple1 ((triple4 ((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((triple1 ((triple4 ((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
((triple4) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((triple4 triple3) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple4 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
((triple13) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
((triple11) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
((triple11 triple10) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple8 triple9) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple11 ((triple11) -> (rule8 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple13) -> (rule5 % int2)) triple9) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Harry is rough.
("Harry" "is" "rough" "+")
triple16
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple7) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple9) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple9 triple12) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple9 ((triple11 triple10) -> (rule2 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple9 ((triple8 triple9) -> (rule3 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
((triple9 ((triple11 ((triple11) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((triple9 ((((triple13) -> (rule5 % int3)) triple9) -> (rule3 % int2))) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
((((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3
((((((triple7) -> (rule5 % int4))) -> (rule4 % int3)) ((((triple7) -> (rule5 % int4)) ((((triple7) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is cold.
("Fiona" "is" "cold" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple7) -> (rule5 % int3)) ((((triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
int3