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