Erin is big. Erin is furry. Fiona is nice. If Fiona is big and Fiona is smart then Fiona is nice. All nice people are big. Big, smart people are nice. All furry people are smart. Smart people are big. If someone is furry and nice then they are white. If someone is blue and white then they are big. Cold, big people are furry.
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If Fiona is big and Fiona is smart then Fiona is nice.
((("Fiona" "is" "big" "+") ("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "nice" "+"))
All nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Big, smart people are nice.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If someone is furry and nice then they are white.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is blue and white then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Cold, big people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Fiona is nice.
True
1
proof
[(triple3)]
("Fiona" "is" "nice" "+")
triple3
Erin is not big.
False
1
inv-proof
[(triple1 OR ((((triple2) -> rule4)) -> rule5))]
("Erin" "is" "big" "-")
triple1
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Fiona is big.
True
2
proof
[(((triple3) -> rule2))]
("Fiona" "is" "big" "+")
((triple3) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple3) -> rule2))]
("Fiona" "is" "big" "-")
((triple3) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Erin is nice.
True
4
proof
[(((triple1 ((triple2) -> rule4)) -> rule3) OR ((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule3))]
("Erin" "is" "nice" "+")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int3))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not nice.
False
4
inv-proof
[(((triple1 ((triple2) -> rule4)) -> rule3) OR ((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule3))]
("Erin" "is" "nice" "-")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int3))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is white.
True
6
proof
[(((triple2 ((triple1 ((triple2) -> rule4)) -> rule3)) -> rule6) OR ((triple2 ((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule3)) -> rule6))]
("Erin" "is" "white" "+")
((triple2 ((triple1 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((triple2 ((((((triple2) -> (rule4 % int4))) -> (rule5 % int3)) ((triple2) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is not white.
False
6
inv-proof
[(((triple2 ((triple1 ((triple2) -> rule4)) -> rule3)) -> rule6) OR ((triple2 ((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule3)) -> rule6))]
("Erin" "is" "white" "-")
((triple2 ((triple1 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((triple2 ((((((triple2) -> (rule4 % int4))) -> (rule5 % int3)) ((triple2) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is furry.
Unknown
rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "furry" "+")
Fiona is not white.
Unknown
inv-rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("Fiona" "is" "white" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Erin is big.[(triple1 OR ((((triple2) -> rule4)) -> rule5))] Erin is furry.[(triple2)] Fiona is nice.[(triple3)] @1: Erin is smart.[(((triple2) -> rule4))] Fiona is big.[(((triple3) -> rule2))] @2: Erin is nice.[(((triple1 ((triple2) -> rule4)) -> rule3) OR ((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule3))] @3: Erin is white.[(((triple2 ((triple1 ((triple2) -> rule4)) -> rule3)) -> rule6) OR ((triple2 ((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule3)) -> rule6))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple3) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple1 ((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int3))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple2 ((triple1 ((triple2) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((triple2 ((((((triple2) -> (rule4 % int4))) -> (rule5 % int3)) ((triple2) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4