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