Bob is cold. Bob is red. Dave is not big. Dave is nice. Gary is rough. Gary is smart. Gary is young. Rough, red people are not smart. Rough, nice people are smart. All nice people are not red. If Bob is young then Bob is big. If someone is big and not red then they are cold. If someone is rough and nice then they are not cold. Cold people are young. All nice people are young.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Rough, red people are not smart.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "-"))
Rough, nice people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
All nice people are not red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "-"))
If Bob is young then Bob is big.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "big" "+"))
If someone is big and not red then they are cold.
((("someone" "is" "big" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "cold" "+"))
If someone is rough and nice then they are not cold.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "-"))
Cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Gary is not rough.
False
1
inv-proof
[(triple5)]
("Gary" "is" "rough" "-")
triple5
Dave is not red.
True
2
proof
[(((triple4) -> rule3))]
("Dave" "is" "red" "-")
((triple4) -> (rule3 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Bob is not young.
False
2
inv-proof
[(((triple1) -> rule7))]
("Bob" "is" "young" "-")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is big.
True
3
proof
[(((((triple1) -> rule7)) -> rule4))]
("Bob" "is" "big" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule4))]
("Bob" "is" "big" "-")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "cold" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "smart" "+")
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Bob is cold.[(triple1)] Bob is red.[(triple2)] Dave is nice.[(triple4)] Dave is not big.[(triple3)] Gary is rough.[(triple5)] Gary is smart.[(triple6)] Gary is young.[(triple7)] @1: Bob is young.[(((triple1) -> rule7))] Dave is not red.[(((triple4) -> rule3))] Dave is young.[(((triple4) -> rule8))] @2: Bob is big.[(((((triple1) -> rule7)) -> rule4))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is not big.
("Dave" "is" "big" "-")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
((triple4) -> (rule3 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple4) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2