Anne is blue. Anne is cold. Harry is cold. Harry is kind. Harry is rough. Harry is round. Harry is young. If Anne is young then Anne is round. Young things are round. Blue things are big. If something is cold and kind then it is young. If Anne is round and Anne is rough then Anne is cold. Big things are kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If Anne is young then Anne is round.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "round" "+"))
Young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is cold and kind then it is young.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If Anne is round and Anne is rough then Anne is cold.
((("Anne" "is" "round" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "cold" "+"))
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Harry is cold.
True
1
proof
[(triple3)]
("Harry" "is" "cold" "+")
triple3
Harry is not kind.
False
1
inv-proof
[(triple4)]
("Harry" "is" "kind" "-")
triple4
Anne is big.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "big" "-")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
True
5
proof
[(((triple2 ((((triple1) -> rule3)) -> rule6)) -> rule4))]
("Anne" "is" "young" "+")
((triple2 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not young.
False
5
inv-proof
[(((triple2 ((((triple1) -> rule3)) -> rule6)) -> rule4))]
("Anne" "is" "young" "-")
((triple2 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "big" "-")
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 cold.[(triple2)] Harry is cold.[(triple3)] Harry is kind.[(triple4)] Harry is rough.[(triple5)] Harry is round.[(triple6 OR ((triple7) -> rule2) OR ((((triple3 triple4) -> rule4)) -> rule2))] Harry is young.[(triple7 OR ((triple3 triple4) -> rule4))] @1: Anne is big.[(((triple1) -> rule3))] @2: Anne is kind.[(((((triple1) -> rule3)) -> rule6))] @3: Anne is young.[(((triple2 ((((triple1) -> rule3)) -> rule6)) -> rule4))] @4: Anne is round.[(((((triple2 ((((triple1) -> rule3)) -> rule6)) -> rule4)) -> rule1) OR ((((triple2 ((((triple1) -> rule3)) -> rule6)) -> rule4)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is rough.
("Harry" "is" "rough" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
((triple7) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple3 triple4) -> (rule4 % int2))) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple7
((triple3 triple4) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((triple2 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((((triple2 ((((triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
((((triple2 ((((triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4