Anne is green. Anne is kind. Bob is cold. Bob is green. Bob is quiet. Bob is smart. Harry is big. Harry is green. Harry is quiet. Harry is smart. All kind people are blue. If someone is smart and green then they are cold. All cold people are kind.
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart and green then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Bob is green.
True
1
proof
[(triple4)]
("Bob" "is" "green" "+")
triple4
Bob is not smart.
False
1
inv-proof
[(triple6)]
("Bob" "is" "smart" "-")
triple6
Anne is blue.
True
2
proof
[(((triple2) -> rule1))]
("Anne" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple3) -> rule3) OR ((((triple6 triple4) -> rule2)) -> rule3))]
("Bob" "is" "kind" "-")
((triple3) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple6 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is green.[(triple1)] Anne is kind.[(triple2)] Bob is cold.[(triple3 OR ((triple6 triple4) -> rule2))] Bob is green.[(triple4)] Bob is quiet.[(triple5)] Bob is smart.[(triple6)] Harry is big.[(triple7)] Harry is green.[(triple8)] Harry is quiet.[(triple9)] Harry is smart.[(triple10)] @1: Anne is blue.[(((triple2) -> rule1))] Bob is kind.[(((triple3) -> rule3) OR ((((triple6 triple4) -> rule2)) -> rule3))] Harry is cold.[(((triple10 triple8) -> rule2))] @2: Bob is blue.[(((((triple3) -> rule3)) -> rule1) OR ((((((triple6 triple4) -> rule2)) -> rule3)) -> rule1))] Harry is kind.[(((((triple10 triple8) -> rule2)) -> rule3))] @3: Harry is blue.[(((((((triple10 triple8) -> rule2)) -> rule3)) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
((triple6 triple4) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple6 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple10 triple8) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple6 triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
((((triple10 triple8) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple10 triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3