Anne is big. Anne is green. Anne is nice. Anne is red. Bob is cold. Bob is green. Bob is nice. Bob is red. Bob is round. Fiona is round. Gary is cold. Gary is green. All green things are cold. Blue, big things are not round. If something is big then it is round. All big things are green. All cold, big things are green. If Bob is blue then Bob is not nice. If Gary is cold then Gary is big. If something is red and not round then it is nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Blue, big things are not round.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "round" "-"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All cold, big things are green.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Bob is blue then Bob is not nice.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "nice" "-"))
If Gary is cold then Gary is big.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "big" "+"))
If something is red and not round then it is nice.
((("something" "is" "red" "+") ("something" "is" "round" "~")) -> ("something" "is" "nice" "+"))
Bob is cold.
True
1
proof
[(triple5 OR ((triple6) -> rule1))]
("Bob" "is" "cold" "+")
triple5
((triple6) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is cold.
True
2
proof
[(((triple2) -> rule1) OR ((((triple1) -> rule4)) -> rule1))]
("Anne" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not cold.
False
2
inv-proof
[(((triple2) -> rule1) OR ((((triple1) -> rule4)) -> rule1))]
("Anne" "is" "cold" "-")
((triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "nice" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "green" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2 OR ((triple1) -> rule4))] Anne is nice.[(triple3)] Anne is red.[(triple4)] Bob is cold.[(triple5 OR ((triple6) -> rule1))] Bob is green.[(triple6)] Bob is nice.[(triple7)] Bob is red.[(triple8)] Bob is round.[(triple9)] Fiona is round.[(triple10)] Gary is cold.[(triple11 OR ((triple12) -> rule1))] Gary is green.[(triple12 OR ((((triple11) -> rule7)) -> rule4) OR ((triple11 ((triple11) -> rule7)) -> rule5))] @1: Anne is cold.[(((triple2) -> rule1) OR ((((triple1) -> rule4)) -> rule1))] Anne is round.[(((triple1) -> rule3))] Gary is big.[(((triple11) -> rule7) OR ((((triple12) -> rule1)) -> rule7))] @2: Gary is round.[(((((triple11) -> rule7)) -> rule3) OR ((((((triple12) -> rule1)) -> rule7)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple1) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
triple5
((triple6) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple6
Bob is nice.
("Bob" "is" "nice" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
triple8
Bob is round.
("Bob" "is" "round" "+")
triple9
Fiona is round.
("Fiona" "is" "round" "+")
triple10
Gary is cold.
("Gary" "is" "cold" "+")
triple11
((triple12) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple12
((((triple11) -> (rule7 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((triple11 ((triple11) -> (rule7 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple11) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule7 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((((triple11) -> (rule7 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((((triple12) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3