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