Anne is green. Anne is round. Bob is blue. Bob is green. Bob is red. Harry is kind. Harry is round. Rough things are big. Kind, red things are round. All green things are kind.
Anne is green.
("Anne" "is" "green" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Kind, red things are round.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Bob is red.
True
1
proof
[(triple5)]
("Bob" "is" "red" "+")
triple5
Bob is not red.
False
1
inv-proof
[(triple5)]
("Bob" "is" "red" "-")
triple5
Bob is kind.
True
2
proof
[(((triple4) -> rule3))]
("Bob" "is" "kind" "+")
((triple4) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple4) -> rule3))]
("Bob" "is" "kind" "-")
((triple4) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
True
4
proof
[(((((triple4) -> rule3) triple5) -> rule2))]
("Bob" "is" "round" "+")
((((triple4) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not round.
False
4
inv-proof
[(((((triple4) -> rule3) triple5) -> rule2))]
("Bob" "is" "round" "-")
((((triple4) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "big" "+")
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is green.[(triple1)] Anne is round.[(triple2)] Bob is blue.[(triple3)] Bob is green.[(triple4)] Bob is red.[(triple5)] Harry is kind.[(triple6)] Harry is round.[(triple7)] @1: Anne is kind.[(((triple1) -> rule3))] Bob is kind.[(((triple4) -> rule3))] @2: Bob is round.[(((((triple4) -> rule3) triple5) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple4) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple4) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2