Bob is big. Dave is nice. Dave is red. If Bob is nice and Bob is red then Bob is big. Big, quiet people are cold. If someone is young then they are big. All cold, red people are big. All big, young people are red. If someone is quiet then they are young. If someone is nice then they are big. If Bob is big and Bob is quiet then Bob is young.
Bob is big.
("Bob" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
If Bob is nice and Bob is red then Bob is big.
((("Bob" "is" "nice" "+") ("Bob" "is" "red" "+")) -> ("Bob" "is" "big" "+"))
Big, quiet people are cold.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is young then they are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
All cold, red people are big.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
All big, young people are red.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If Bob is big and Bob is quiet then Bob is young.
((("Bob" "is" "big" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "young" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple3)]
("Dave" "is" "red" "-")
triple3
Dave is big.
True
2
proof
[(((triple2) -> rule7))]
("Dave" "is" "big" "+")
((triple2) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple2) -> rule7))]
("Dave" "is" "big" "-")
((triple2) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "young" "-")
Bob is red.
Unknown
rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Bob" "is" "red" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is big.[(triple1)] Dave is nice.[(triple2)] Dave is red.[(triple3)] @1: Dave is big.[(((triple2) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule7 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1