Anne is green. Anne is smart. Bob is nice. Bob is red. Bob is rough. Bob is young. Charlie is cold. Charlie is green. Harry is cold. Harry is green. Harry is rough. Harry is smart. All young people are rough. All red people are nice. If someone is smart then they are red. All smart, nice people are cold. Cold, green people are young. All young people are cold.
Anne is green.
("Anne" "is" "green" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart then they are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
All smart, nice people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Cold, green people are young.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Bob is nice.
True
1
proof
[(triple3 OR ((triple4) -> rule2))]
("Bob" "is" "nice" "+")
triple3
((triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule2))]
("Bob" "is" "nice" "-")
triple3
((triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Harry is young.
True
3
proof
[(((triple9 triple10) -> rule5) OR ((((triple12 ((((triple12) -> rule3)) -> rule2)) -> rule4) triple10) -> rule5))]
("Harry" "is" "young" "+")
((triple9 triple10) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple12 ((((triple12) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Bob is not cold.
False
2
inv-proof
[(((triple6) -> rule6))]
("Bob" "is" "cold" "-")
((triple6) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Harry is nice.
True
3
proof
[(((((triple12) -> rule3)) -> rule2))]
("Harry" "is" "nice" "+")
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Charlie is not rough.
False
4
inv-proof
[(((((triple7 triple8) -> rule5)) -> rule1))]
("Charlie" "is" "rough" "-")
((((triple7 triple8) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Anne is cold.
True
5
proof
[(((triple2 ((((triple2) -> rule3)) -> rule2)) -> rule4))]
("Anne" "is" "cold" "+")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is not cold.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule3)) -> rule2)) -> rule4))]
("Anne" "is" "cold" "-")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is young.
True
7
proof
[(((((triple2 ((((triple2) -> rule3)) -> rule2)) -> rule4) triple1) -> rule5))]
("Anne" "is" "young" "+")
((((triple2 ((((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is not young.
False
7
inv-proof
[(((((triple2 ((((triple2) -> rule3)) -> rule2)) -> rule4) triple1) -> rule5))]
("Anne" "is" "young" "-")
((((triple2 ((((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is rough.
True
8
proof
[(((((((triple2 ((((triple2) -> rule3)) -> rule2)) -> rule4) triple1) -> rule5)) -> rule1))]
("Anne" "is" "rough" "+")
((((((triple2 ((((triple2) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5
Anne is not rough.
False
8
inv-proof
[(((((((triple2 ((((triple2) -> rule3)) -> rule2)) -> rule4) triple1) -> rule5)) -> rule1))]
("Anne" "is" "rough" "-")
((((((triple2 ((((triple2) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Anne is green.[(triple1)] Anne is smart.[(triple2)] Bob is nice.[(triple3 OR ((triple4) -> rule2))] Bob is red.[(triple4)] Bob is rough.[(triple5 OR ((triple6) -> rule1))] Bob is young.[(triple6)] Charlie is cold.[(triple7)] Charlie is green.[(triple8)] Harry is cold.[(triple9 OR ((triple12 ((((triple12) -> rule3)) -> rule2)) -> rule4))] Harry is green.[(triple10)] Harry is rough.[(triple11 OR ((((triple9 triple10) -> rule5)) -> rule1) OR ((((((triple12 ((((triple12) -> rule3)) -> rule2)) -> rule4) triple10) -> rule5)) -> rule1))] Harry is smart.[(triple12)] @1: Anne is red.[(((triple2) -> rule3))] Bob is cold.[(((triple6) -> rule6))] Charlie is young.[(((triple7 triple8) -> rule5))] Harry is red.[(((triple12) -> rule3))] Harry is young.[(((triple9 triple10) -> rule5) OR ((((triple12 ((((triple12) -> rule3)) -> rule2)) -> rule4) triple10) -> rule5))] @2: Anne is nice.[(((((triple2) -> rule3)) -> rule2))] Charlie is rough.[(((((triple7 triple8) -> rule5)) -> rule1))] Harry is nice.[(((((triple12) -> rule3)) -> rule2))] @3: Anne is cold.[(((triple2 ((((triple2) -> rule3)) -> rule2)) -> rule4))] @4: Anne is young.[(((((triple2 ((((triple2) -> rule3)) -> rule2)) -> rule4) triple1) -> rule5))] @5: Anne is rough.[(((((((triple2 ((((triple2) -> rule3)) -> rule2)) -> rule4) triple1) -> rule5)) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple4) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple6) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
((triple12 ((((triple12) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
((((triple9 triple10) -> (rule5 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((((triple12 ((((triple12) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) triple10) -> (rule5 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
int5
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Anne is red.
("Anne" "is" "red" "+")
((triple2) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple6) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple7 triple8) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple12) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple9 triple10) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple12 ((((triple12) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple7 triple8) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((((triple2 ((((triple2) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple2 ((((triple2) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5