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