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