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