Bob is quiet. Charlie is not furry. Charlie is quiet. Harry is big. Harry is cold. Harry is furry. Harry is quiet. If Bob is young then Bob is not blue. Young, big things are blue. All quiet things are big. If something is cold then it is quiet. If Harry is not furry and Harry is not blue then Harry is rough. If Bob is not rough and Bob is not big then Bob is furry.
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Bob is young then Bob is not blue.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "blue" "-"))
Young, big things are blue.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is cold then it is quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If Harry is not furry and Harry is not blue then Harry is rough.
((("Harry" "is" "furry" "~") ("Harry" "is" "blue" "~")) -> ("Harry" "is" "rough" "+"))
If Bob is not rough and Bob is not big then Bob is furry.
((("Bob" "is" "rough" "~") ("Bob" "is" "big" "~")) -> ("Bob" "is" "furry" "+"))
Harry is quiet.
True
1
proof
[(triple7 OR ((triple5) -> rule4))]
("Harry" "is" "quiet" "+")
triple7
((triple5) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Charlie is furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "+")
triple2
Charlie is big.
True
2
proof
[(((triple3) -> rule3))]
("Charlie" "is" "big" "+")
((triple3) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "big" "-")
((triple1) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "rough" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is quiet.[(triple1)] Charlie is not furry.[(triple2)] Charlie is quiet.[(triple3)] Harry is big.[(triple4 OR ((triple7) -> rule3) OR ((((triple5) -> rule4)) -> rule3))] Harry is cold.[(triple5)] Harry is furry.[(triple6)] Harry is quiet.[(triple7 OR ((triple5) -> rule4))] @1: Bob is big.[(((triple1) -> rule3))] Charlie is big.[(((triple3) -> rule3))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
((triple7) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
((triple5) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple3) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1