Charlie is rough. Dave is quiet. Dave is red. Dave is white. Erin is big. Erin is quiet. Erin is red. Erin is rough. Erin is white. Harry is big. Harry is furry. Harry is kind. Harry is quiet. Harry is red. Harry is white. Big people are rough. If Harry is kind then Harry is furry. All rough people are big. If Erin is white and Erin is furry then Erin is rough. If someone is quiet and furry then they are white. If Erin is furry and Erin is big then Erin is rough. If someone is quiet and red then they are big. Rough, big people are red.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If Harry is kind then Harry is furry.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "furry" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If Erin is white and Erin is furry then Erin is rough.
((("Erin" "is" "white" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "rough" "+"))
If someone is quiet and furry then they are white.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If Erin is furry and Erin is big then Erin is rough.
((("Erin" "is" "furry" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "rough" "+"))
If someone is quiet and red then they are big.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Rough, big people are red.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Erin is quiet.
True
1
proof
[(triple6)]
("Erin" "is" "quiet" "+")
triple6
Dave is not quiet.
False
1
inv-proof
[(triple2)]
("Dave" "is" "quiet" "-")
triple2
Dave is big.
True
3
proof
[(((triple2 triple3) -> rule7))]
("Dave" "is" "big" "+")
((triple2 triple3) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "big" "-")
((triple1) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is rough.
True
4
proof
[(((((triple2 triple3) -> rule7)) -> rule1))]
("Dave" "is" "rough" "+")
((((triple2 triple3) -> (rule7 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Charlie is not red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule8))]
("Charlie" "is" "red" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "white" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Charlie is rough.[(triple1)] Dave is quiet.[(triple2)] Dave is red.[(triple3)] Dave is white.[(triple4)] Erin is big.[(triple5 OR ((triple8) -> rule3) OR ((triple6 triple7) -> rule7))] Erin is quiet.[(triple6)] Erin is red.[(triple7 OR ((triple8 triple5) -> rule8) OR ((triple8 ((triple8) -> rule3)) -> rule8) OR ((((triple5) -> rule1) triple5) -> rule8) OR ((((triple5) -> rule1) ((triple8) -> rule3)) -> rule8))] Erin is rough.[(triple8 OR ((triple5) -> rule1) OR ((((triple6 triple7) -> rule7)) -> rule1))] Erin is white.[(triple9)] Harry is big.[(triple10 OR ((triple13 triple14) -> rule7))] Harry is furry.[(triple11 OR ((triple12) -> rule2))] Harry is kind.[(triple12)] Harry is quiet.[(triple13)] Harry is red.[(triple14 OR ((((triple10) -> rule1) triple10) -> rule8))] Harry is white.[(triple15 OR ((triple13 triple11) -> rule5) OR ((triple13 ((triple12) -> rule2)) -> rule5))] @1: Charlie is big.[(((triple1) -> rule3))] Dave is big.[(((triple2 triple3) -> rule7))] Harry is rough.[(((triple10) -> rule1) OR ((((triple13 triple14) -> rule7)) -> rule1))] @2: Charlie is red.[(((triple1 ((triple1) -> rule3)) -> rule8))] Dave is rough.[(((((triple2 triple3) -> rule7)) -> rule1))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
((triple8) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple6 triple7) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Erin is red.
("Erin" "is" "red" "+")
triple7
((triple8 triple5) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple8 ((triple8) -> (rule3 % int2))) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple5) -> (rule1 % int2)) triple5) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((triple5) -> (rule1 % int3)) ((triple8) -> (rule3 % int2))) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
triple8
((triple5) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple6 triple7) -> (rule7 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
((triple13 triple14) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple11
((triple12) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
((((triple10) -> (rule1 % int2)) triple10) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple13 triple11) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple13 ((triple12) -> (rule2 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple2 triple3) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple13 triple14) -> (rule7 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2 triple3) -> (rule7 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2