Dave is quiet. Dave is smart. Fiona is green. Cold people are green. If someone is white then they are quiet. If someone is smart and quiet then they are green. If someone is smart and cold then they are green. If someone is big then they are white. Green people are big. If Fiona is cold and Fiona is quiet then Fiona is white. All young people are cold.
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart and quiet then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and cold then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If Fiona is cold and Fiona is quiet then Fiona is white.
((("Fiona" "is" "cold" "+") ("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "white" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Dave is smart.
True
1
proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Fiona is not green.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "green" "-")
triple3
Dave is green.
True
3
proof
[(((triple2 triple1) -> rule3))]
("Dave" "is" "green" "+")
((triple2 triple1) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not green.
False
3
inv-proof
[(((triple2 triple1) -> rule3))]
("Dave" "is" "green" "-")
((triple2 triple1) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Fiona is white.
True
3
proof
[(((((triple3) -> rule6)) -> rule5))]
("Fiona" "is" "white" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Dave is not big.
False
4
inv-proof
[(((((triple2 triple1) -> rule3)) -> rule6))]
("Dave" "is" "big" "-")
((((triple2 triple1) -> (rule3 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Fiona is quiet.
True
4
proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule2))]
("Fiona" "is" "quiet" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not quiet.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule2))]
("Fiona" "is" "quiet" "-")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "cold" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Dave is quiet.[(triple1)] Dave is smart.[(triple2)] Fiona is green.[(triple3)] @1: Dave is green.[(((triple2 triple1) -> rule3))] Fiona is big.[(((triple3) -> rule6))] @2: Dave is big.[(((((triple2 triple1) -> rule3)) -> rule6))] Fiona is white.[(((((triple3) -> rule6)) -> rule5))] @3: Dave is white.[(((((((triple2 triple1) -> rule3)) -> rule6)) -> rule5))] Fiona is quiet.[(((((((triple3) -> rule6)) -> rule5)) -> rule2))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
((triple2 triple1) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule6 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple2 triple1) -> (rule3 % int2))) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((((triple2 triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3