Dave is quiet. Erin is big. Fiona is red. Harry is red. If someone is quiet then they are round. All nice people are round. Red, big people are not round. If Harry is round then Harry is red. If Erin is quiet then Erin is round. If someone is quiet and not white then they are cold. Quiet, big people are cold. If someone is round then they are big.
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is big.
("Erin" "is" "big" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is red.
("Harry" "is" "red" "+")
If someone is quiet then they are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Red, big people are not round.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "-"))
If Harry is round then Harry is red.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "red" "+"))
If Erin is quiet then Erin is round.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "round" "+"))
If someone is quiet and not white then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "cold" "+"))
Quiet, big people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
Fiona is red.
True
1
proof
[(triple3)]
("Fiona" "is" "red" "+")
triple3
Fiona is not red.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "red" "-")
triple3
Dave is round.
True
2
proof
[(((triple1) -> rule1))]
("Dave" "is" "round" "+")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "round" "-")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule8))]
("Dave" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule8))]
("Dave" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule8)) -> rule7))]
("Dave" "is" "cold" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is not cold.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule8)) -> rule7))]
("Dave" "is" "cold" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is big.
Unknown
rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Harry" "is" "big" "+")
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is big.
Unknown
rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Fiona" "is" "big" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Dave is quiet.[(triple1)] Erin is big.[(triple2)] Fiona is red.[(triple3)] Harry is red.[(triple4)] @1: Dave is round.[(((triple1) -> rule1))] @2: Dave is big.[(((((triple1) -> rule1)) -> rule8))] @3: Dave is cold.[(((triple1 ((((triple1) -> rule1)) -> rule8)) -> rule7))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3