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