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