Bob is cold. Bob is quiet. Bob is not white. Bob is young. Charlie is big. Charlie is cold. Charlie is nice. Charlie is smart. Charlie is young. Dave is big. Dave is quiet. Dave is young. Gary is quiet. Gary is smart. Gary is young. If someone is cold and nice then they are big. All big people are smart. If someone is nice and quiet then they are cold. All quiet people are cold. If Dave is nice and Dave is white then Dave is cold. If someone is big and cold then they are young. If someone is big and not cold then they are not young. If Bob is big and Bob is not young then Bob is smart.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not white.
("Bob" "is" "white" "-")
Bob is young.
("Bob" "is" "young" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is cold and nice then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
All big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is nice and quiet then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
All quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If Dave is nice and Dave is white then Dave is cold.
((("Dave" "is" "nice" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "cold" "+"))
If someone is big and cold then they are young.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is big and not cold then they are not young.
((("someone" "is" "big" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "young" "-"))
If Bob is big and Bob is not young then Bob is smart.
((("Bob" "is" "big" "+") ("Bob" "is" "young" "~")) -> ("Bob" "is" "smart" "+"))
Bob is cold.
True
1
proof
[(triple1 OR ((triple2) -> rule4))]
("Bob" "is" "cold" "+")
triple1
((triple2) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
False
1
inv-proof
[(triple3)]
("Bob" "is" "white" "+")
triple3
Gary is cold.
True
2
proof
[(((triple13) -> rule4))]
("Gary" "is" "cold" "+")
((triple13) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple11) -> rule4))]
("Dave" "is" "cold" "-")
((triple11) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "smart" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is cold.[(triple1 OR ((triple2) -> rule4))] Bob is not white.[(triple3)] Bob is quiet.[(triple2)] Bob is young.[(triple4)] Charlie is big.[(triple5 OR ((triple6 triple7) -> rule1))] Charlie is cold.[(triple6)] Charlie is nice.[(triple7)] Charlie is smart.[(triple8 OR ((triple5) -> rule2) OR ((((triple6 triple7) -> rule1)) -> rule2))] Charlie is young.[(triple9 OR ((triple5 triple6) -> rule6) OR ((((triple6 triple7) -> rule1) triple6) -> rule6))] Dave is big.[(triple10)] Dave is quiet.[(triple11)] Dave is young.[(triple12 OR ((triple10 ((triple11) -> rule4)) -> rule6))] Gary is quiet.[(triple13)] Gary is smart.[(triple14)] Gary is young.[(triple15)] @1: Dave is cold.[(((triple11) -> rule4))] Dave is smart.[(((triple10) -> rule2))] Gary is cold.[(((triple13) -> rule4))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple2) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not white.
("Bob" "is" "white" "-")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
((triple6 triple7) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is nice.
("Charlie" "is" "nice" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
triple8
((triple5) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((triple6 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple9
((triple5 triple6) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple6 triple7) -> (rule1 % int2)) triple6) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
triple10
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
((triple10 ((triple11) -> (rule4 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple14
Gary is young.
("Gary" "is" "young" "+")
triple15
Dave is cold.
("Dave" "is" "cold" "+")
((triple11) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple10) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple13) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1