Fiona is big. Fiona is smart. Gary is big. Gary is quiet. Gary is round. Gary is white. Harry is not cold. All smart, big people are red. If Gary is red then Gary is cold. If Harry is not cold then Harry is red. All quiet people are smart. If Harry is not quiet then Harry is white. If someone is round and not red then they are not white. If someone is cold and red then they are round. If someone is quiet and not smart then they are round.
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
All smart, big people are red.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If Gary is red then Gary is cold.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "cold" "+"))
If Harry is not cold then Harry is red.
((("Harry" "is" "cold" "~")) -> ("Harry" "is" "red" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If Harry is not quiet then Harry is white.
((("Harry" "is" "quiet" "~")) -> ("Harry" "is" "white" "+"))
If someone is round and not red then they are not white.
((("someone" "is" "round" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "white" "-"))
If someone is cold and red then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is quiet and not smart then they are round.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "round" "+"))
Harry is not cold.
True
1
proof
[(triple7)]
("Harry" "is" "cold" "-")
triple7
Fiona is not smart.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "smart" "-")
triple2
Fiona is red.
True
3
proof
[(((triple2 triple1) -> rule1))]
("Fiona" "is" "red" "+")
((triple2 triple1) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple4) -> rule4))]
("Gary" "is" "smart" "-")
((triple4) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
True
4
proof
[(((((triple4) -> rule4) triple3) -> rule1))]
("Gary" "is" "red" "+")
((((triple4) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not red.
False
4
inv-proof
[(((((triple4) -> rule4) triple3) -> rule1))]
("Gary" "is" "red" "-")
((((triple4) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
True
5
proof
[(((((((triple4) -> rule4) triple3) -> rule1)) -> rule2))]
("Gary" "is" "cold" "+")
((((((triple4) -> (rule4 % int3)) triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not cold.
False
5
inv-proof
[(((((((triple4) -> rule4) triple3) -> rule1)) -> rule2))]
("Gary" "is" "cold" "-")
((((((triple4) -> (rule4 % int3)) triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "round" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "white" "+")
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "round" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Fiona is big.[(triple1)] Fiona is smart.[(triple2)] Gary is big.[(triple3)] Gary is quiet.[(triple4)] Gary is round.[(triple5 OR ((((((((triple4) -> rule4) triple3) -> rule1)) -> rule2) ((((triple4) -> rule4) triple3) -> rule1)) -> rule7))] Gary is white.[(triple6)] Harry is not cold.[(triple7)] @1: Fiona is red.[(((triple2 triple1) -> rule1))] Gary is smart.[(((triple4) -> rule4))] Harry is red.[(((triple7) -> rule3))] @2: Gary is red.[(((((triple4) -> rule4) triple3) -> rule1))] @3: Gary is cold.[(((((((triple4) -> rule4) triple3) -> rule1)) -> rule2))]
Fiona is big.
("Fiona" "is" "big" "+")
triple1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
((((((((triple4) -> (rule4 % int4)) triple3) -> (rule1 % int3))) -> (rule2 % int2)) ((((triple4) -> (rule4 % int4)) triple3) -> (rule1 % int3))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
triple6
Harry is not cold.
("Harry" "is" "cold" "-")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
((triple2 triple1) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple4) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple7) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((((triple4) -> (rule4 % int2)) triple3) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple4) -> (rule4 % int3)) triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3