Anne is not cold. Anne is red. Anne is rough. Anne is white. Bob is cold. Erin is not rough. Harry is white. If Erin is green and Erin is red then Erin is rough. All cold, red things are young. Rough things are not young. If something is big and rough then it is white. If something is young and cold then it is white. All young, white things are green. All cold things are red. Green, white things are not big. Big, white things are not cold.
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Harry is white.
("Harry" "is" "white" "+")
If Erin is green and Erin is red then Erin is rough.
((("Erin" "is" "green" "+") ("Erin" "is" "red" "+")) -> ("Erin" "is" "rough" "+"))
All cold, red things are young.
((("something" "is" "cold" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Rough things are not young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "-"))
If something is big and rough then it is white.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If something is young and cold then it is white.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
All young, white things are green.
((("something" "is" "young" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Green, white things are not big.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "-"))
Big, white things are not cold.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "cold" "-"))
Harry is white.
True
1
proof
[(triple7)]
("Harry" "is" "white" "+")
triple7
Anne is cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Bob is red.
True
2
proof
[(((triple5) -> rule7))]
("Bob" "is" "red" "+")
((triple5) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple5) -> rule7))]
("Bob" "is" "red" "-")
((triple5) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
True
4
proof
[(((triple5 ((triple5) -> rule7)) -> rule2))]
("Bob" "is" "young" "+")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not young.
False
4
inv-proof
[(((triple5 ((triple5) -> rule7)) -> rule2))]
("Bob" "is" "young" "-")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
True
6
proof
[(((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5))]
("Bob" "is" "white" "+")
((((triple5 ((triple5) -> (rule7 % int3))) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not white.
False
6
inv-proof
[(((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5))]
("Bob" "is" "white" "-")
((((triple5 ((triple5) -> (rule7 % int3))) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
True
11
proof
[(((((triple5 ((triple5) -> rule7)) -> rule2) ((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5)) -> rule6))]
("Bob" "is" "green" "+")
((((triple5 ((triple5) -> (rule7 % int4))) -> (rule2 % int3)) ((((triple5 ((triple5) -> (rule7 % int4))) -> (rule2 % int3)) triple5) -> (rule5 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is not green.
False
11
inv-proof
[(((((triple5 ((triple5) -> rule7)) -> rule2) ((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5)) -> rule6))]
("Bob" "is" "green" "-")
((((triple5 ((triple5) -> (rule7 % int4))) -> (rule2 % int3)) ((((triple5 ((triple5) -> (rule7 % int4))) -> (rule2 % int3)) triple5) -> (rule5 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is not big.
True
18
proof
[(((((((triple5 ((triple5) -> rule7)) -> rule2) ((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5)) -> rule6) ((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5)) -> rule8))]
("Bob" "is" "big" "-")
((((((triple5 ((triple5) -> (rule7 % int5))) -> (rule2 % int4)) ((((triple5 ((triple5) -> (rule7 % int5))) -> (rule2 % int4)) triple5) -> (rule5 % int3))) -> (rule6 % int2)) ((((triple5 ((triple5) -> (rule7 % int5))) -> (rule2 % int4)) triple5) -> (rule5 % int3))) -> (rule8 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
Bob is big.
False
18
inv-proof
[(((((((triple5 ((triple5) -> rule7)) -> rule2) ((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5)) -> rule6) ((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5)) -> rule8))]
("Bob" "is" "big" "+")
((((((triple5 ((triple5) -> (rule7 % int5))) -> (rule2 % int4)) ((((triple5 ((triple5) -> (rule7 % int5))) -> (rule2 % int4)) triple5) -> (rule5 % int3))) -> (rule6 % int2)) ((((triple5 ((triple5) -> (rule7 % int5))) -> (rule2 % int4)) triple5) -> (rule5 % int3))) -> (rule8 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
Harry is not green.
Unknown
inv-rconc
[@2: Harry is green.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Harry" "is" "green" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "green" "+")
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "young" "-")
Erin is young.
Unknown
rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "young" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "white" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is not cold.[(triple1)] Anne is red.[(triple2)] Anne is rough.[(triple3)] Anne is white.[(triple4)] Bob is cold.[(triple5)] Erin is not rough.[(triple6)] Harry is white.[(triple7)] @1: Anne is not young.[(((triple3) -> rule3))] Bob is red.[(((triple5) -> rule7))] @2: Bob is young.[(((triple5 ((triple5) -> rule7)) -> rule2))] @3: Bob is white.[(((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5))] @4: Bob is green.[(((((triple5 ((triple5) -> rule7)) -> rule2) ((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5)) -> rule6))] @5: Bob is not big.[(((((((triple5 ((triple5) -> rule7)) -> rule2) ((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5)) -> rule6) ((((triple5 ((triple5) -> rule7)) -> rule2) triple5) -> rule5)) -> rule8))]
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
triple5
Erin is not rough.
("Erin" "is" "rough" "-")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Anne is not young.
("Anne" "is" "young" "-")
((triple3) -> (rule3 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple5) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple5 ((triple5) -> (rule7 % int3))) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
((((triple5 ((triple5) -> (rule7 % int4))) -> (rule2 % int3)) ((((triple5 ((triple5) -> (rule7 % int4))) -> (rule2 % int3)) triple5) -> (rule5 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Bob is not big.
("Bob" "is" "big" "-")
((((((triple5 ((triple5) -> (rule7 % int5))) -> (rule2 % int4)) ((((triple5 ((triple5) -> (rule7 % int5))) -> (rule2 % int4)) triple5) -> (rule5 % int3))) -> (rule6 % int2)) ((((triple5 ((triple5) -> (rule7 % int5))) -> (rule2 % int4)) triple5) -> (rule5 % int3))) -> (rule8 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5