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