Bob is big. Bob is nice. Bob is red. Bob is round. Bob is smart. Bob is young. Dave is nice. Fiona is big. Fiona is red. Harry is big. Harry is cold. Harry is nice. Harry is red. Harry is round. Harry is smart. All nice people are red. Red people are young.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All nice people are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Bob is red.
True
1
proof
[(triple3 OR ((triple2) -> rule1))]
("Bob" "is" "red" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is not round.
False
1
inv-proof
[(triple14)]
("Harry" "is" "round" "-")
triple14
Dave is red.
True
2
proof
[(((triple7) -> rule1))]
("Dave" "is" "red" "+")
((triple7) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple7) -> rule1))]
("Dave" "is" "red" "-")
((triple7) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
True
3
proof
[(((((triple7) -> rule1)) -> rule2))]
("Dave" "is" "young" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not young.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule2))]
("Dave" "is" "young" "-")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is nice.[(triple2)] Bob is red.[(triple3 OR ((triple2) -> rule1))] Bob is round.[(triple4)] Bob is smart.[(triple5)] Bob is young.[(triple6 OR ((triple3) -> rule2) OR ((((triple2) -> rule1)) -> rule2))] Dave is nice.[(triple7)] Fiona is big.[(triple8)] Fiona is red.[(triple9)] Harry is big.[(triple10)] Harry is cold.[(triple11)] Harry is nice.[(triple12)] Harry is red.[(triple13 OR ((triple12) -> rule1))] Harry is round.[(triple14)] Harry is smart.[(triple15)] @1: Dave is red.[(((triple7) -> rule1))] Fiona is young.[(((triple9) -> rule2))] Harry is young.[(((triple13) -> rule2) OR ((((triple12) -> rule1)) -> rule2))] @2: Dave is young.[(((((triple7) -> rule1)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
((triple3) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Fiona is big.
("Fiona" "is" "big" "+")
triple8
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
((triple12) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Dave is red.
("Dave" "is" "red" "+")
((triple7) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple9) -> (rule2 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple13) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2