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