Bob is big. Bob is blue. Bob is cold. Charlie is blue. Charlie is furry. Charlie is rough. Charlie is young. Gary is big. Gary is blue. Gary is cold. Gary is furry. Gary is round. Gary is young. Harry is big. Harry is blue. Harry is furry. Young people are furry. If Gary is rough and Gary is blue then Gary is round. If someone is furry and rough then they are blue. All big people are round. If someone is round and cold then they are young. Big people are blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Young people are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If Gary is rough and Gary is blue then Gary is round.
((("Gary" "is" "rough" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "round" "+"))
If someone is furry and rough then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is round and cold then they are young.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
Harry is big.
True
1
proof
[(triple14)]
("Harry" "is" "big" "+")
triple14
Bob is not blue.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule6))]
("Bob" "is" "blue" "-")
triple2
((triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple14) -> rule4))]
("Harry" "is" "round" "-")
((triple14) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is young.
True
4
proof
[(((((triple1) -> rule4) triple3) -> rule5))]
("Bob" "is" "young" "+")
((((triple1) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not young.
False
4
inv-proof
[(((((triple1) -> rule4) triple3) -> rule5))]
("Bob" "is" "young" "-")
((((triple1) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "round" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2 OR ((triple1) -> rule6))] Bob is cold.[(triple3)] Charlie is blue.[(triple4 OR ((triple5 triple6) -> rule3) OR ((((triple7) -> rule1) triple6) -> rule3))] Charlie is furry.[(triple5 OR ((triple7) -> rule1))] Charlie is rough.[(triple6)] Charlie is young.[(triple7)] Gary is big.[(triple8)] Gary is blue.[(triple9 OR ((triple8) -> rule6))] Gary is cold.[(triple10)] Gary is furry.[(triple11 OR ((triple13) -> rule1) OR ((((triple12 triple10) -> rule5)) -> rule1) OR ((((((triple8) -> rule4) triple10) -> rule5)) -> rule1))] Gary is round.[(triple12 OR ((triple8) -> rule4))] Gary is young.[(triple13 OR ((triple12 triple10) -> rule5) OR ((((triple8) -> rule4) triple10) -> rule5))] Harry is big.[(triple14)] Harry is blue.[(triple15 OR ((triple14) -> rule6))] Harry is furry.[(triple16)] @1: Bob is round.[(((triple1) -> rule4))] Harry is round.[(((triple14) -> rule4))] @2: Bob is young.[(((((triple1) -> rule4) triple3) -> rule5))] @3: Bob is furry.[(((((((triple1) -> rule4) triple3) -> rule5)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple1) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
((triple5 triple6) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple7) -> (rule1 % int2)) triple6) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple5
((triple7) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
((triple8) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Gary is furry.
("Gary" "is" "furry" "+")
triple11
((triple13) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple12 triple10) -> (rule5 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((((((triple8) -> (rule4 % int3)) triple10) -> (rule5 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
triple12
((triple8) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple13
((triple12 triple10) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple8) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple14
Harry is blue.
("Harry" "is" "blue" "+")
triple15
((triple14) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple16
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple14) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple1) -> (rule4 % int3)) triple3) -> (rule5 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3