Dave is green. Dave is quiet. Dave is smart. Fiona is cold. Fiona is nice. Gary is cold. Gary is green. Gary is quiet. Gary is round. Gary is white. If Dave is nice then Dave is quiet. All smart things are green. All green things are smart. Round things are green. Nice, round things are white. All green, round things are quiet. If something is cold and nice then it is green. Round, white things are quiet.
Dave is green.
("Dave" "is" "green" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If Dave is nice then Dave is quiet.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "quiet" "+"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All green things are smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Nice, round things are white.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All green, round things are quiet.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If something is cold and nice then it is green.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Round, white things are quiet.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Gary is white.
True
1
proof
[(triple10)]
("Gary" "is" "white" "+")
triple10
Gary is not white.
False
1
inv-proof
[(triple10)]
("Gary" "is" "white" "-")
triple10
Gary is smart.
True
2
proof
[(((triple7) -> rule3) OR ((((triple9) -> rule4)) -> rule3))]
("Gary" "is" "smart" "+")
((triple7) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Fiona is not green.
False
3
inv-proof
[(((triple4 triple5) -> rule7))]
("Fiona" "is" "green" "-")
((triple4 triple5) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "white" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "white" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Dave is green.[(triple1 OR ((triple3) -> rule2))] Dave is quiet.[(triple2)] Dave is smart.[(triple3 OR ((triple1) -> rule3))] Fiona is cold.[(triple4)] Fiona is nice.[(triple5)] Gary is cold.[(triple6)] Gary is green.[(triple7 OR ((triple9) -> rule4))] Gary is quiet.[(triple8 OR ((triple7 triple9) -> rule6) OR ((triple9 triple10) -> rule8) OR ((((triple9) -> rule4) triple9) -> rule6))] Gary is round.[(triple9)] Gary is white.[(triple10)] @1: Fiona is green.[(((triple4 triple5) -> rule7))] Gary is smart.[(((triple7) -> rule3) OR ((((triple9) -> rule4)) -> rule3))] @2: Fiona is smart.[(((((triple4 triple5) -> rule7)) -> rule3))]
Dave is green.
("Dave" "is" "green" "+")
triple1
((triple3) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
((triple1) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Gary is cold.
("Gary" "is" "cold" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple9) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
((triple7 triple9) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((triple9 triple10) -> (rule8 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple9) -> (rule4 % int2)) triple9) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Fiona is green.
("Fiona" "is" "green" "+")
((triple4 triple5) -> (rule7 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple4 triple5) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2