Anne is round. Bob is cold. Bob is kind. Fiona is young. Harry is blue. Harry is round. Harry is white. If something is big then it is round. All big things are young. If Anne is round then Anne is big.
Anne is round.
("Anne" "is" "round" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If Anne is round then Anne is big.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "big" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Bob is not cold.
False
1
inv-proof
[(triple2)]
("Bob" "is" "cold" "-")
triple2
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 young.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "young" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "young" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "round" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Anne is round.[(triple1)] Bob is cold.[(triple2)] Bob is kind.[(triple3)] Fiona is young.[(triple4)] Harry is blue.[(triple5)] Harry is round.[(triple6)] Harry is white.[(triple7)] @1: Anne is big.[(((triple1) -> rule3))] @2: Anne is young.[(((((triple1) -> rule3)) -> rule2))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Fiona is young.
("Fiona" "is" "young" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2