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