Bob is cold. Bob is quiet. Bob is red. Dave is cold. Dave is young. Gary is big. Gary is quiet. Gary is not red. Gary is round. Gary is young. Harry is not quiet. Harry is not round. All red, smart people are round. Red people are smart.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not red.
("Gary" "is" "red" "-")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is not round.
("Harry" "is" "round" "-")
All red, smart people are round.
((("someone" "is" "red" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Gary is round.
True
1
proof
[(triple9)]
("Gary" "is" "round" "+")
triple9
Gary is red.
False
1
inv-proof
[(triple8)]
("Gary" "is" "red" "+")
triple8
Bob is smart.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "smart" "-")
((triple3) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
True
4
proof
[(((triple3 ((triple3) -> rule2)) -> rule1))]
("Bob" "is" "round" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not round.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule1))]
("Bob" "is" "round" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Bob is cold.[(triple1)] Bob is quiet.[(triple2)] Bob is red.[(triple3)] Dave is cold.[(triple4)] Dave is young.[(triple5)] Gary is big.[(triple6)] Gary is not red.[(triple8)] Gary is quiet.[(triple7)] Gary is round.[(triple9)] Gary is young.[(triple10)] Harry is not quiet.[(triple11)] Harry is not round.[(triple12)] @1: Bob is smart.[(((triple3) -> rule2))] @2: Bob is round.[(((triple3 ((triple3) -> rule2)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is not red.
("Gary" "is" "red" "-")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple11
Harry is not round.
("Harry" "is" "round" "-")
triple12
Bob is smart.
("Bob" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2