Bob is nice. Bob is red. Bob is round. Bob is smart. Charlie is quiet. Charlie is red. Charlie is smart. Dave is big. Dave is blue. Dave is nice. Dave is quiet. Dave is not red. Dave is not round. Dave is smart. Erin is nice. Erin is round. Quiet things are smart. Red, big things are smart. All round things are red. Blue, nice things are not red. All red things are big. If something is red then it is big. If something is nice and not quiet then it is round. If Charlie is nice and Charlie is not big then Charlie is smart.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not round.
("Dave" "is" "round" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Red, big things are smart.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Blue, nice things are not red.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "-"))
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is nice and not quiet then it is round.
((("something" "is" "nice" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "round" "+"))
If Charlie is nice and Charlie is not big then Charlie is smart.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "big" "~")) -> ("Charlie" "is" "smart" "+"))
Dave is nice.
True
1
proof
[(triple10)]
("Dave" "is" "nice" "+")
triple10
Dave is not big.
False
1
inv-proof
[(triple8)]
("Dave" "is" "big" "-")
triple8
Charlie is big.
True
2
proof
[(((triple6) -> rule5) OR ((triple6) -> rule6))]
("Charlie" "is" "big" "+")
((triple6) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple6) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple2) -> rule5) OR ((triple2) -> rule6) OR ((((triple3) -> rule3)) -> rule5) OR ((((triple3) -> rule3)) -> rule6))]
("Bob" "is" "big" "-")
((triple2) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple2) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Erin is big.
True
3
proof
[(((((triple16) -> rule3)) -> rule5) OR ((((triple16) -> rule3)) -> rule6))]
("Erin" "is" "big" "+")
((((triple16) -> (rule3 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple16) -> (rule3 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not big.
False
3
inv-proof
[(((((triple16) -> rule3)) -> rule5) OR ((((triple16) -> rule3)) -> rule6))]
("Erin" "is" "big" "-")
((((triple16) -> (rule3 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple16) -> (rule3 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
True
6
proof
[(((((triple16) -> rule3) ((((triple16) -> rule3)) -> rule5)) -> rule2) OR ((((triple16) -> rule3) ((((triple16) -> rule3)) -> rule6)) -> rule2))]
("Erin" "is" "smart" "+")
((((triple16) -> (rule3 % int3)) ((((triple16) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple16) -> (rule3 % int3)) ((((triple16) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not smart.
False
6
inv-proof
[(((((triple16) -> rule3) ((((triple16) -> rule3)) -> rule5)) -> rule2) OR ((((triple16) -> rule3) ((((triple16) -> rule3)) -> rule6)) -> rule2))]
("Erin" "is" "smart" "-")
((((triple16) -> (rule3 % int3)) ((((triple16) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple16) -> (rule3 % int3)) ((((triple16) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "round" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is nice.[(triple1)] Bob is red.[(triple2 OR ((triple3) -> rule3))] Bob is round.[(triple3)] Bob is smart.[(triple4 OR ((triple2 ((triple2) -> rule5)) -> rule2) OR ((triple2 ((triple2) -> rule6)) -> rule2) OR ((((triple3) -> rule3) ((triple2) -> rule5)) -> rule2) OR ((((triple3) -> rule3) ((triple2) -> rule6)) -> rule2) OR ((triple2 ((((triple3) -> rule3)) -> rule5)) -> rule2) OR ((triple2 ((((triple3) -> rule3)) -> rule6)) -> rule2) OR ((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule2) OR ((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule6)) -> rule2))] Charlie is quiet.[(triple5)] Charlie is red.[(triple6)] Charlie is smart.[(triple7 OR ((triple5) -> rule1) OR ((triple6 ((triple6) -> rule5)) -> rule2) OR ((triple6 ((triple6) -> rule6)) -> rule2))] Dave is big.[(triple8)] Dave is blue.[(triple9)] Dave is nice.[(triple10)] Dave is not red.[(triple12 OR ((triple9 triple10) -> rule4))] Dave is not round.[(triple13)] Dave is quiet.[(triple11)] Dave is smart.[(triple14 OR ((triple11) -> rule1))] Erin is nice.[(triple15)] Erin is round.[(triple16)] @1: Bob is big.[(((triple2) -> rule5) OR ((triple2) -> rule6) OR ((((triple3) -> rule3)) -> rule5) OR ((((triple3) -> rule3)) -> rule6))] Charlie is big.[(((triple6) -> rule5) OR ((triple6) -> rule6))] Erin is red.[(((triple16) -> rule3))] @2: Erin is big.[(((((triple16) -> rule3)) -> rule5) OR ((((triple16) -> rule3)) -> rule6))] @3: Erin is smart.[(((((triple16) -> rule3) ((((triple16) -> rule3)) -> rule5)) -> rule2) OR ((((triple16) -> rule3) ((((triple16) -> rule3)) -> rule6)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
((triple3) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((triple2 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((triple2 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((triple3) -> (rule3 % int3)) ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple3) -> (rule3 % int3)) ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((triple2 ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((triple2 ((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
((triple5) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple6 ((triple6) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple6 ((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is nice.
("Dave" "is" "nice" "+")
triple10
Dave is not red.
("Dave" "is" "red" "-")
triple12
((triple9 triple10) -> (rule4 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is not round.
("Dave" "is" "round" "-")
triple13
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple14
((triple11) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple15
Erin is round.
("Erin" "is" "round" "+")
triple16
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((triple2) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((triple6) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple6) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple16) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple16) -> (rule3 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple16) -> (rule3 % int2))) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((triple16) -> (rule3 % int3)) ((((triple16) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
((((triple16) -> (rule3 % int3)) ((((triple16) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3