Anne is smart. Bob is smart. Erin is not cold. Fiona is white. If someone is cold and rough then they are red. If someone is white then they are rough. If Erin is smart and Erin is white then Erin is rough. If Fiona is big then Fiona is cold. All smart people are not big. If someone is rough then they are smart.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Fiona is white.
("Fiona" "is" "white" "+")
If someone is cold and rough then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If Erin is smart and Erin is white then Erin is rough.
((("Erin" "is" "smart" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "rough" "+"))
If Fiona is big then Fiona is cold.
((("Fiona" "is" "big" "+")) -> ("Fiona" "is" "cold" "+"))
All smart people are not big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "-"))
If someone is rough then they are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Erin is not cold.
True
1
proof
[(triple3)]
("Erin" "is" "cold" "-")
triple3
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Fiona is rough.
True
2
proof
[(((triple4) -> rule2))]
("Fiona" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Bob is big.
False
2
inv-proof
[(((triple2) -> rule5))]
("Bob" "is" "big" "+")
((triple2) -> (rule5 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Fiona is smart.
True
3
proof
[(((((triple4) -> rule2)) -> rule6))]
("Fiona" "is" "smart" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule6))]
("Fiona" "is" "smart" "-")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not big.
True
4
proof
[(((((((triple4) -> rule2)) -> rule6)) -> rule5))]
("Fiona" "is" "big" "-")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is not big.
("Fiona" "is" "big" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is big.
False
4
inv-proof
[(((((((triple4) -> rule2)) -> rule6)) -> rule5))]
("Fiona" "is" "big" "+")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is not big.
("Fiona" "is" "big" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not red.
Unknown
inv-rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Fiona" "is" "red" "-")
Erin is smart.
Unknown
rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "red" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Anne is smart.[(triple1)] Bob is smart.[(triple2)] Erin is not cold.[(triple3)] Fiona is white.[(triple4)] @1: Anne is not big.[(((triple1) -> rule5))] Bob is not big.[(((triple2) -> rule5))] Fiona is rough.[(((triple4) -> rule2))] @2: Fiona is smart.[(((((triple4) -> rule2)) -> rule6))] @3: Fiona is not big.[(((((((triple4) -> rule2)) -> rule6)) -> rule5))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Erin is not cold.
("Erin" "is" "cold" "-")
triple3
Fiona is white.
("Fiona" "is" "white" "+")
triple4
Anne is not big.
("Anne" "is" "big" "-")
((triple1) -> (rule5 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Bob is not big.
("Bob" "is" "big" "-")
((triple2) -> (rule5 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple4) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not big.
("Fiona" "is" "big" "-")
((((((triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Fiona is not big.
("Fiona" "is" "big" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3