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