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