Charlie is blue. Charlie is green. Charlie is nice. Charlie is round. Charlie is young. Dave is blue. Dave is green. Dave is nice. Dave is red. Dave is round. Dave is white. Dave is young. Fiona is blue. Harry is nice. Harry is white. If something is green and red then it is white. All nice things are blue. All green, young things are nice. If Harry is blue then Harry is green. All blue, white things are green. If something is round and young then it is blue. All blue, red things are nice. Green, red things are young.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is green and red then it is white.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All green, young things are nice.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If Harry is blue then Harry is green.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "green" "+"))
All blue, white things are green.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is round and young then it is blue.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All blue, red things are nice.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Green, red things are young.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Dave is blue.
True
1
proof
[(triple6 OR ((triple8) -> rule2) OR ((triple10 triple12) -> rule6) OR ((((triple7 triple12) -> rule3)) -> rule2) OR ((triple10 ((triple7 triple9) -> rule8)) -> rule6) OR ((((triple7 ((triple7 triple9) -> rule8)) -> rule3)) -> rule2))]
("Dave" "is" "blue" "+")
triple6
((triple8) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple10 triple12) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple7 triple12) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple10 ((triple7 triple9) -> (rule8 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple7 ((triple7 triple9) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Charlie is not young.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "young" "-")
triple5
Harry is blue.
True
2
proof
[(((triple14) -> rule2))]
("Harry" "is" "blue" "+")
((triple14) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple14) -> rule2))]
("Harry" "is" "blue" "-")
((triple14) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
True
3
proof
[(((((triple14) -> rule2)) -> rule4) OR ((((triple14) -> rule2) triple15) -> rule5))]
("Harry" "is" "green" "+")
((((triple14) -> (rule2 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple14) -> (rule2 % int2)) triple15) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not green.
False
3
inv-proof
[(((((triple14) -> rule2)) -> rule4) OR ((((triple14) -> rule2) triple15) -> rule5))]
("Harry" "is" "green" "-")
((((triple14) -> (rule2 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple14) -> (rule2 % int2)) triple15) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Fiona is not nice.
Unknown
inv-rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "young" "+")
Fiona is not green.
Unknown
inv-rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Fiona" "is" "green" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is blue.[(triple1 OR ((triple3) -> rule2) OR ((triple4 triple5) -> rule6) OR ((((triple2 triple5) -> rule3)) -> rule2))] Charlie is green.[(triple2)] Charlie is nice.[(triple3 OR ((triple2 triple5) -> rule3))] Charlie is round.[(triple4)] Charlie is young.[(triple5)] Dave is blue.[(triple6 OR ((triple8) -> rule2) OR ((triple10 triple12) -> rule6) OR ((((triple7 triple12) -> rule3)) -> rule2) OR ((triple10 ((triple7 triple9) -> rule8)) -> rule6) OR ((((triple7 ((triple7 triple9) -> rule8)) -> rule3)) -> rule2))] Dave is green.[(triple7 OR ((triple6 triple11) -> rule5) OR ((((triple8) -> rule2) triple11) -> rule5) OR ((((triple10 triple12) -> rule6) triple11) -> rule5))] Dave is nice.[(triple8 OR ((triple6 triple9) -> rule7) OR ((triple7 triple12) -> rule3) OR ((triple7 ((triple7 triple9) -> rule8)) -> rule3) OR ((((triple10 triple12) -> rule6) triple9) -> rule7) OR ((((triple6 triple11) -> rule5) triple12) -> rule3) OR ((((triple6 triple11) -> rule5) ((triple7 triple9) -> rule8)) -> rule3) OR ((triple7 ((((triple6 triple11) -> rule5) triple9) -> rule8)) -> rule3) OR ((((triple10 ((triple7 triple9) -> rule8)) -> rule6) triple9) -> rule7) OR ((((((triple10 triple12) -> rule6) triple11) -> rule5) triple12) -> rule3) OR ((((triple6 triple11) -> rule5) ((((triple6 triple11) -> rule5) triple9) -> rule8)) -> rule3) OR ((((((triple10 triple12) -> rule6) triple11) -> rule5) ((triple7 triple9) -> rule8)) -> rule3) OR ((((((triple10 triple12) -> rule6) triple11) -> rule5) ((((triple6 triple11) -> rule5) triple9) -> rule8)) -> rule3))] Dave is red.[(triple9)] Dave is round.[(triple10)] Dave is white.[(triple11 OR ((triple7 triple9) -> rule1))] Dave is young.[(triple12 OR ((triple7 triple9) -> rule8) OR ((((triple6 triple11) -> rule5) triple9) -> rule8) OR ((((((triple8) -> rule2) triple11) -> rule5) triple9) -> rule8))] Fiona is blue.[(triple13)] Harry is nice.[(triple14)] Harry is white.[(triple15)] @1: Harry is blue.[(((triple14) -> rule2))] @2: Harry is green.[(((((triple14) -> rule2)) -> rule4) OR ((((triple14) -> rule2) triple15) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple3) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple4 triple5) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple2 triple5) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
((triple2 triple5) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
((triple8) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple10 triple12) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple7 triple12) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple10 ((triple7 triple9) -> (rule8 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple7 ((triple7 triple9) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
triple7
((triple6 triple11) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple8) -> (rule2 % int2)) triple11) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple10 triple12) -> (rule6 % int2)) triple11) -> (rule5 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple8
((triple6 triple9) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple7 triple12) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple7 ((triple7 triple9) -> (rule8 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple10 triple12) -> (rule6 % int2)) triple9) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple6 triple11) -> (rule5 % int2)) triple12) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple6 triple11) -> (rule5 % int3)) ((triple7 triple9) -> (rule8 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((triple7 ((((triple6 triple11) -> (rule5 % int3)) triple9) -> (rule8 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((triple10 ((triple7 triple9) -> (rule8 % int3))) -> (rule6 % int2)) triple9) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((triple10 triple12) -> (rule6 % int3)) triple11) -> (rule5 % int2)) triple12) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((triple6 triple11) -> (rule5 % int3)) ((((triple6 triple11) -> (rule5 % int3)) triple9) -> (rule8 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
((((((triple10 triple12) -> (rule6 % int4)) triple11) -> (rule5 % int3)) ((triple7 triple9) -> (rule8 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
((((((triple10 triple12) -> (rule6 % int4)) triple11) -> (rule5 % int3)) ((((triple6 triple11) -> (rule5 % int3)) triple9) -> (rule8 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
((triple7 triple9) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple12
((triple7 triple9) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple6 triple11) -> (rule5 % int2)) triple9) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((((triple8) -> (rule2 % int3)) triple11) -> (rule5 % int2)) triple9) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple13
Harry is nice.
("Harry" "is" "nice" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Harry is blue.
("Harry" "is" "blue" "+")
((triple14) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple14) -> (rule2 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple14) -> (rule2 % int2)) triple15) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2