Bob is cold. Bob is furry. Bob is quiet. Bob is red. Bob is rough. Charlie is big. Charlie is cold. Charlie is furry. Charlie is green. Charlie is quiet. Harry is furry. Harry is red. If Bob is big then Bob is not cold. All quiet things are rough. If Harry is cold then Harry is red. If something is big and not rough then it is cold. If something is quiet and not big then it is cold. Furry things are cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
If Bob is big then Bob is not cold.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "cold" "-"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If Harry is cold then Harry is red.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "red" "+"))
If something is big and not rough then it is cold.
((("something" "is" "big" "+") ("something" "is" "rough" "~")) -> ("something" "is" "cold" "+"))
If something is quiet and not big then it is cold.
((("something" "is" "quiet" "+") ("something" "is" "big" "~")) -> ("something" "is" "cold" "+"))
Furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Charlie is quiet.
True
1
proof
[(triple10)]
("Charlie" "is" "quiet" "+")
triple10
Harry is not red.
False
1
inv-proof
[(triple12 OR ((((triple11) -> rule6)) -> rule3))]
("Harry" "is" "red" "-")
triple12
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Bob is cold.[(triple1 OR ((triple2) -> rule6))] Bob is furry.[(triple2)] Bob is quiet.[(triple3)] Bob is red.[(triple4)] Bob is rough.[(triple5 OR ((triple3) -> rule2))] Charlie is big.[(triple6)] Charlie is cold.[(triple7 OR ((triple8) -> rule6))] Charlie is furry.[(triple8)] Charlie is green.[(triple9)] Charlie is quiet.[(triple10)] Harry is furry.[(triple11)] Harry is red.[(triple12 OR ((((triple11) -> rule6)) -> rule3))] @1: Charlie is rough.[(((triple10) -> rule2))] Harry is cold.[(((triple11) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple2) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
((triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
((triple8) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
((((triple11) -> (rule6 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple10) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple11) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1