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